-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
↳ QTRS
↳ AAECC Innermost
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
-1(s(x), s(y)) → -1(x, y)
F(s(x)) → -1(p(*(s(x), s(x))), *(s(x), s(x)))
F(s(x)) → F(-(p(*(s(x), s(x))), *(s(x), s(x))))
F(s(x)) → P(*(s(x), s(x)))
F(s(x)) → *1(s(x), s(x))
+1(s(x), y) → +1(x, y)
*1(x, s(y)) → *1(x, y)
*1(x, s(y)) → +1(x, *(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
-1(s(x), s(y)) → -1(x, y)
F(s(x)) → -1(p(*(s(x), s(x))), *(s(x), s(x)))
F(s(x)) → F(-(p(*(s(x), s(x))), *(s(x), s(x))))
F(s(x)) → P(*(s(x), s(x)))
F(s(x)) → *1(s(x), s(x))
+1(s(x), y) → +1(x, y)
*1(x, s(y)) → *1(x, y)
*1(x, s(y)) → +1(x, *(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
+1(s(x), y) → +1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
+1(s(x), y) → +1(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
+1(s(x), y) → +1(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
*1(x, s(y)) → *1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
*1(x, s(y)) → *1(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
*1(x, s(y)) → *1(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
-1(s(x), s(y)) → -1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
-1(s(x), s(y)) → -1(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
-1(s(x), s(y)) → -1(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
F(s(x)) → F(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
f(s(x)) → f(-(p(*(s(x), s(x))), *(s(x), s(x))))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F(s(x)) → F(-(p(*(s(x), s(x))), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
f(s(x0))
f(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
F(s(x)) → F(-(p(*(s(x), s(x))), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
F(s(x)) → F(-(p(+(s(x), *(s(x), x))), *(s(x), s(x))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(x)) → F(-(p(+(s(x), *(s(x), x))), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
F(s(x)) → F(-(p(s(+(x, *(s(x), x)))), *(s(x), s(x))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(x)) → F(-(p(s(+(x, *(s(x), x)))), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
F(s(x)) → F(-(+(x, *(s(x), x)), *(s(x), s(x))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
F(s(x)) → F(-(+(x, *(s(x), x)), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
p(s(x)) → x
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F(s(x)) → F(-(+(x, *(s(x), x)), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
p(s(x0))
p(s(x0))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
F(s(x)) → F(-(+(x, *(s(x), x)), *(s(x), s(x))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(x)) → F(-(+(x, *(s(x), x)), +(s(x), *(s(x), x))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(x)) → F(-(+(x, *(s(x), x)), +(s(x), *(s(x), x))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(x)) → F(-(+(x, *(s(x), x)), s(+(x, *(s(x), x)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
F(s(x)) → F(-(+(x, *(s(x), x)), s(+(x, *(s(x), x)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(0)) → F(-(+(0, *(s(0), 0)), s(+(0, 0))))
F(s(s(x1))) → F(-(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(s(x1))) → F(-(+(s(x1), *(s(s(x1)), s(x1))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(0)) → F(-(+(0, 0), s(+(0, *(s(0), 0)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
F(s(0)) → F(-(+(0, 0), s(+(0, *(s(0), 0)))))
F(s(s(x1))) → F(-(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(0)) → F(-(+(0, *(s(0), 0)), s(+(0, 0))))
F(s(s(x1))) → F(-(+(s(x1), *(s(s(x1)), s(x1))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(0)) → F(-(*(s(0), 0), s(+(0, 0))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(0)) → F(-(*(s(0), 0), s(+(0, 0))))
F(s(0)) → F(-(+(0, 0), s(+(0, *(s(0), 0)))))
F(s(s(x1))) → F(-(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(s(x1))) → F(-(+(s(x1), *(s(s(x1)), s(x1))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(0)) → F(-(*(s(0), 0), s(+(0, 0))))
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(0)) → F(-(+(0, 0), s(+(0, *(s(0), 0)))))
F(s(s(x1))) → F(-(+(s(x1), *(s(s(x1)), s(x1))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(0)) → F(-(*(s(0), 0), s(+(0, 0))))
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(0)) → F(-(+(0, 0), s(+(0, *(s(0), 0)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(0)) → F(-(0, s(+(0, *(s(0), 0)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
F(s(0)) → F(-(0, s(+(0, *(s(0), 0)))))
F(s(0)) → F(-(*(s(0), 0), s(+(0, 0))))
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
F(s(0)) → F(-(*(s(0), 0), s(+(0, 0))))
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(0)) → F(-(0, s(+(0, 0))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(0)) → F(-(0, s(+(0, 0))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(s(x1))) → F(-(s(+(x1, +(s(s(x1)), *(s(s(x1)), x1)))), s(+(s(x1), *(s(s(x1)), s(x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, +(s(s(x1)), *(s(s(x1)), x1))), +(s(x1), *(s(s(x1)), s(x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(s(+(x1, *(s(s(x1)), s(x1)))), s(+(s(x1), +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(s(x1))) → F(-(+(x1, +(s(s(x1)), *(s(s(x1)), x1))), +(s(x1), *(s(s(x1)), s(x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, *(s(s(x1)), s(x1))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, *(s(s(x1)), s(x1))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
F(s(s(x1))) → F(-(+(x1, +(s(s(x1)), *(s(s(x1)), x1))), +(s(x1), *(s(s(x1)), s(x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(+(s(x1), *(s(s(x1)), x1)))), +(s(x1), *(s(s(x1)), s(x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(+(s(x1), *(s(s(x1)), x1)))), +(s(x1), *(s(s(x1)), s(x1)))))
F(s(s(x1))) → F(-(+(x1, *(s(s(x1)), s(x1))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, +(s(s(x1)), *(s(s(x1)), x1))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(+(s(x1), *(s(s(x1)), x1)))), +(s(x1), *(s(s(x1)), s(x1)))))
F(s(s(x1))) → F(-(+(x1, +(s(s(x1)), *(s(s(x1)), x1))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), +(s(x1), *(s(s(x1)), s(x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), +(s(x1), *(s(s(x1)), s(x1)))))
F(s(s(x1))) → F(-(+(x1, +(s(s(x1)), *(s(s(x1)), x1))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(+(s(x1), *(s(s(x1)), x1)))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), +(s(x1), *(s(s(x1)), s(x1)))))
F(s(s(x1))) → F(-(+(x1, s(+(s(x1), *(s(s(x1)), x1)))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, *(s(s(x1)), s(x1))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, *(s(s(x1)), s(x1))))))
F(s(s(x1))) → F(-(+(x1, s(+(s(x1), *(s(s(x1)), x1)))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, *(s(s(x1)), s(x1))))))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, +(s(s(x1)), *(s(s(x1)), x1))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, +(s(s(x1)), *(s(s(x1)), x1))))))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), +(s(x1), +(s(s(x1)), *(s(s(x1)), x1)))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, +(s(s(x1)), *(s(s(x1)), x1))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, +(s(s(x1)), *(s(s(x1)), x1))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, s(+(s(x1), *(s(s(x1)), x1)))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, s(+(s(x1), *(s(s(x1)), x1)))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, s(s(+(x1, *(s(s(x1)), x1))))))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ MNOCProof
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, s(s(+(x1, *(s(s(x1)), x1))))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ MNOCProof
↳ QDP
F(s(s(x1))) → F(-(+(x1, s(s(+(x1, *(s(s(x1)), x1))))), s(+(x1, s(s(+(x1, *(s(s(x1)), x1))))))))
*(x, s(y)) → +(x, *(x, y))
*(x, 0) → 0
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)